Section:
Software
AAC_tactics
Participants :
Thomas Braibant, Damien Pous [correspondant] .
AAC_tactics is a plugin for the Coq proof-assistant that implements new proof tactics for rewriting modulo associativity and commutativity.
It is available at http://sardes.inrialpes.fr/~braibant/aac_tactics
and as part of the Coq distribution.
ACM: D.2.4 Software/Program Verification
Keywords: Rewriting, rewriting modulo AC, proof tactics, proof assistant
Software benefit: AAC_tactics provides novel efficient proof tactics for rewriting modulo associativity and commutativity.
License: LGPL
Type of human computer interaction: N/A
OS/Middleware: Windows, Linux, MacOS X
Programming language: Coq